loc:Id, ds:x:Id fp Type, knd:Knd, T:Type, x:Id,
f:((State(ds)TDeclaredType(ds;x)) + (State(ds)TDeclaredType(ds;x))).
R-Feasible(Reffect(loc;ds;knd;T;x;f))  (x  dom(ds)) 

latex

Definitions	x. t(x), , t  T, P & Q, R-Feasible(R), P  Q, x:A. B(x), x(s), Normal(ds), Normal(T)
Lemmas	fpf wf, Knd wf, rationals wf, decl-type wf, decl-state wf, lnk wf, ldst wf, Id wf, isrcv wf, assert wf, normal-type wf, normal-ds wf, Reffect-domain